Nuprl Lemma : fpf-cap-subtype_functionality
11,40
postcript
pdf
A
:Type,
d1
,
d2
:EqDecider(
A
),
f
:
a
:
A
fp
Type,
x
:
A
,
z
:Type.
f
(
x
)?
z
r
f
(
x
)?
z
latex
Definitions
f
(
x
)?
z
,
a
:
A
fp
B
(
a
)
,
EqDecider(
T
)
,
x
.
t
(
x
)
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
fpf-cap
wf
,
subtype
rel
self
,
deq
wf
,
fpf
wf
,
fpf-cap
functionality
origin
A:Type, d1, d2:EqDecider(A), f:a:A fp
Type, x:A, z:Type. f(x)?z 
r f(x)?z A:Type, d1, d2:EqDecider(A), f:a:A fp Type, x:A, z:Type. f(x)?z r f(x)?z B(a)
x. t(x)x:A. B(x)
T